Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    plus(x,0)  → x
2:    plus(x,s(y))  → s(plus(x,y))
3:    times(0,y)  → 0
4:    times(x,0)  → 0
5:    times(s(x),y)  → plus(times(x,y),y)
6:    p(s(s(x)))  → s(p(s(x)))
7:    p(s(0))  → 0
8:    fac(s(x))  → times(fac(p(s(x))),s(x))
There are 7 dependency pairs:
9:    PLUS(x,s(y))  → PLUS(x,y)
10:    TIMES(s(x),y)  → PLUS(times(x,y),y)
11:    TIMES(s(x),y)  → TIMES(x,y)
12:    P(s(s(x)))  → P(s(x))
13:    FAC(s(x))  → TIMES(fac(p(s(x))),s(x))
14:    FAC(s(x))  → FAC(p(s(x)))
15:    FAC(s(x))  → P(s(x))
The approximated dependency graph contains 4 SCCs: {12}, {9}, {11} and {14}.
Tyrolean Termination Tool  (0.02 seconds)   ---  May 4, 2006